4.3. 宇宙（Universe）🔗

类型由宇宙分类。宇宙有时也称为 类别(sort)。每个宇宙都有一个自然数层级(level)。 Sort 操作符可根据给定层级构造出一个宇宙。若一个宇宙的层级小于另一个，则该宇宙本身也小于后者。除命题外（将在本章后面介绍），某宇宙内的类型只可以对更小宇宙内的类型进行量化。 Sort 0 是命题类型（Prop），而每个 Sort (u + 1) 可描述数据类型。

每个宇宙都是下一个更大宇宙的元素，比如 Sort 5 包含了 Sort 4。所以如下例子有效：

example : Sort 5 := Sort 4
example : Sort 2 := Sort 1

但 Sort 3 不属于 Sort 5：

example : Sort 5 := type mismatch
  Type 2
has type
  Type 3 : Type 4
but is expected to have type
  Type 4 : Type 5Sort 3

type mismatch
  Type 2
has type
  Type 3 : Type 4
but is expected to have type
  Type 4 : Type 5

同理，Unit 属于 Sort 1，不属于 Sort 2：

example : Sort 1 := Unit

example : Sort 2 := type mismatch
  Unit
has type
  Type : Type 1
but is expected to have type
  Type 1 : Type 2Unit

type mismatch
  Unit
has type
  Type : Type 1
but is expected to have type
  Type 1 : Type 2

由于命题和数据类型有不同的用法及不同规则，Lean 提供了缩写 Type 和 Prop 来区分二者。 Type u 是 Sort (u + 1) 的缩写，所以 Type 0 就是 Sort 1，Type 3 就是 Sort 4。 Type 0 还可以简写为 Type，所以 Unit : Type 以及 Type : Type 1 成立。 Prop 是 Sort 0 的缩写。

4.3.1. 直谓性(Predicativity)

每个宇宙都包含依值函数类型，即可以表示全称量化和蕴涵。函数类型的宇宙由其参数类型和返回值类型的宇宙决定；具体规则取决于返回类型是不是命题。

谓词,即返回命题的函数（即结果为 Prop 中类型的函数）可以拥有任意宇宙的参数类型，但这类函数本身还是属于 Prop。换言之，命题具有 非直谓性的(impredicative) 量化，因为命题本身可以是关于所有命题（以及所有其他类型）的陈述。

非直谓性

证明无关性可视为对所有命题进行量化的命题：

example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2

命题同样可以对任意层级的类型做量化：

example : Prop := ∀ (α : Type), ∀ (x : α), x = x
example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x

对于 1 及以上层级（即 Type u 层级）中的宇宙，量化是 直谓性 的。在这一范围内，函数类型所属宇宙为参数类型和返回类型宇宙的最小上界。

函数类型的宇宙层级

下列类型都属于 Type 2：

example (α : Type 1) (β : Type 2) : Type 2 := α → β
example (α : Type 2) (β : Type 1) : Type 2 := α → β

Type 的直谓性

下例会出错，因为 α 的层级大于 1。换句话说，标注的宇宙低于函数类型的宇宙：

example (α : Type 2) (β : Type 1) : Type 1 := type mismatch
  α → β
has type
  Type 2 : Type 3
but is expected to have type
  Type 1 : Type 2α → β

type mismatch
  α → β
has type
  Type 2 : Type 3
but is expected to have type
  Type 1 : Type 2

Lean 的宇宙不是累积性的；也就是说，Type u 中的类型不会自动属于 Type (u + 1)。每个类型只属于唯一一个宇宙。

无累积性

下例不可通过，因为标注的宇宙层级比实际函数类型要大：

example (α : Type 2) (β : Type 1) : Type 3 := type mismatch
  α → β
has type
  Type 2 : Type 3
but is expected to have type
  Type 3 : Type 4α → β

type mismatch
  α → β
has type
  Type 2 : Type 3
but is expected to have type
  Type 3 : Type 4

4.3.2. 多态性（Polymorphism）

Lean 支持 宇宙多态，，即 Lean 环境中的常量可以带有宇宙参数。这些参数可在使用常量时以具体宇宙层级实例化。宇宙参数通过在常量名后以点（dot）加花括号写成。

宇宙多态的身份(identity)函数

完全显式时，身份函数带有宇宙参数 u。其签名为：

id.{u} {α : Sort u} (x : α) : α

宇宙变量还可出现在宇宙层级表达式中，用于为定义中的层级变量提供具体值。多态定义被替换成具体宇宙时，这些表达式也一并被计算成具体数值。

宇宙层级表达式

此例中，Codec 所在宇宙比所含类型的宇宙高 1：

structure Codec.{u} : Type (u + 1) where
  type : Type u
  encode : Array UInt32 → type → Array UInt32
  decode : Array UInt32 → Nat → Option (type × Nat)

Lean 会自动推断大多数层级参数。如下例中无需手工注明 Codec.{0}，因为 Char 属于 Type 0，所以 u 必然为 0：

def Codec.char : Codec where
  type := Char
  encode buf ch := buf.push ch.val
  decode buf i := do
    let v ← buf[i]?
    if h : v.isValidChar then
      let ch : Char := ⟨v, h⟩
      return (ch, i + 1)
    else
      failure

宇宙多态定义实际上创造了一个 严谨的定义，可在不同宇宙层级实例化，不同实例产生的值并不兼容。

宇宙多态与定义等价

如下例中，T 是一个过度宇宙多态的始终返回 true 的函数。由于被标记为 Lean.Parser.Command.declaration : commandopaque，Lean 无法通过展开定义检查等价。尽管两次实例化有同样的参数与类型，但由于宇宙实参不同，它们互不兼容。

opaque T.{u} (_ : Nat) : Bool :=
  (fun (α : Sort u) => true) PUnit.{u}

set_option pp.universes true

def test.{u, v} : T.{u} 0 = T.{v} 0 := type mismatch
  rfl.{?u.29}
has type
  Eq.{?u.29} ?m.31 ?m.31 : Prop
but is expected to have type
  Eq.{1} (T.{u} 0) (T.{v} 0) : Proprfl

type mismatch
  rfl.{?u.29}
has type
  Eq.{?u.29} ?m.31 ?m.31 : Prop
but is expected to have type
  Eq.{1} (T.{u} 0) (T.{v} 0) : Prop

自动绑定的隐式参数会尽可能使用宇宙多态。如下定义身份函数为：

def id' (x : α) := x

results in the signature:

id'.{u} {α : Sort u} (x : α) : α

自动绑定的隐式参数中的相同宇宙

另一方面，由于 Nat 位于 Type 0 宇宙，下例函数自动推导出 α 也位于同一宇宙（因为 m 既应用于 Nat 也应用于 α，二者需同宇宙）：

partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
  if p (← act) then
    return 1 + (← count p act)
  else
    return 0

4.3.2.1. 层级表达式（Level Expressions）🔗

出现在定义中的宇宙层级不限于变量与常量加法，还可使用更复杂的层级表达式进行定义。

Level ::= 0 | 1 | 2 | ...  -- 具体层级
        | u, v             -- 层级变量
        | Level + n        -- 常量加法
        | max Level Level  -- 最小上界
        | imax Level Level -- 非直谓性上界

给定将层级变量赋为具体数值后，计算这些表达式遵循通常的算术规则。 imax 的定义如下：

\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}

imax 用于实现非直谓性的 Prop 量化。具体而言，若 A : Sort u, B : Sort v，则有 (x : A) → B : Sort (imax u v)。若 B : Prop，则函数类型本身为 Prop；否则类型层级为 u 与 v 的最大值。

4.3.2.2. 宇宙变量绑定

宇宙多态定义绑定宇宙变量。这些绑定可以是显式的也可以是隐式的。显式的宇宙变量绑定和实例化发生在定义名称的后缀处。通过在常量名称后加上一个点(.)，然后在花括号中跟随以逗号分隔的宇宙变量序列，来定义或提供宇宙参数。

宇宙多态的 map

如下 map 的声明声明了两个宇宙参数（u 与 v），并实例化多态型 List 各用一次：

def map.{u, v} {α : Type u} {β : Type v}
    (f : α → β) :
    List.{u} α → List.{v} β
  | [] => []
  | x :: xs => f x :: map f xs

就如 Lean 会自动实例化隐式参数，它也会自动实例化宇宙参数。当开启自动插入隐式参数功能（即 autoImplicit 设为 true，默认即如此），无需显式绑定宇宙变量，会自动补全。若设为 false，则需手动写明或用 universe 命令声明。

自动隐式参数与宇宙多态

当 autoImplicit 设为 true（默认设置），该代码可通过，即使没显式绑定宇宙参数：

set_option autoImplicit true
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
  | [] => []
  | x :: xs => f x :: map f xs

设为 false 时，定义因 u、v 不在作用域而报错：

set_option autoImplicit false
def map {α : Type unknown universe level 'u'u} {β : Type unknown universe level 'v'v} (f : α → β) : List α → List β
  | [] => []
  | x :: xs => f x :: map f xs

unknown universe level 'u'

unknown universe level 'v'

除使用 autoImplicit 外，也可以用 universe 命令在特定作用域下声明特定标识符为宇宙变量。

syntax声明宇宙参数

command ::= ...
    | Declares one or more universe variables.

`universe u v`

`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].

Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.

[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)

```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a

/- Implicit type-universe parameter, equivalent to `id₁`.
  Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a

/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```

On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.

```lean
def L₁.{u} := List (Type u)

-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`

universe u
def L₃ := List (Type u)
```

## Examples

```lean
universe u v w

structure Pair (α : Type u) (β : Type v) : Type (max u v) where
  a : α
  b : β

#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
universe ident ident*

声明若干宇宙变量，本作用域内有效。

如同 variable 命令将某标识符视为带类型的参数，universe 命令可以让标识符在后续声明中作为宇宙参数，无需在 autoImplicit 为 true 时显式指明。

autoImplicit = false 时的 universe 命令

set_option autoImplicit false
universe u
def id₃ (α : Type u) (a : α) := a

自动隐式参数功能只会为声明头部中用到的参数插入参数，若宇宙变量只出现在定义右侧而非头部，除非已用 universe 声明，否则即使 autoImplicit 为 true 也不会被自动补齐。

自动宇宙参数与 universe 命令

下定义带显式宇宙参数可通过：

def L.{u} := List (Type u)

即使自动隐式参数开启，下定义因未在头部声明 u 而报错：

set_option autoImplicit true
def L := List (Type unknown universe level 'u'u)

unknown universe level 'u'

用 universe 声明后，右侧用到的 u 可被接受：

universe u
def L := List (Type u)

此时得到的 L 定义是宇宙多态，u 自动插入为宇宙参数。

声明作用域内，若声明和自动参数没用到宇宙变量，定义就不是多态的：

universe u
def L := List (Type 0)
L : Type 1#check L

4.3.2.3. 宇宙提升（Universe Lifting）

当某类型所在宇宙低于实际应用要求时，可以用 宇宙提升 操作符补足。这类操作会用包裹的方式让某类型提升至更高宇宙。主要有两种提升操作：

PLift 可将任意类型（包括命题）提升一级。它可用于将证明项包含进数据结构（如列表）中。
ULift 可将任意非命题类型提升任意层级。

structure

PLift.{u} (α : Sort u) : Type u
PLift.{u} (α : Sort u) : Type u

将一个命题或类型提升到更高的宇宙层级。

PLift α 封装了一个类型为 α 的证明或值。结果类型属于 α 所在宇宙之后的下一个最大宇宙。特别地，命题会变为数据。

相关的类型 ULift 可用于将一个非命题类型的宇宙提升任意多个层级。

示例:

(False : Prop)
(PLift False : Type)
([.up (by trivial), .up (by simp), .up (by decide)] : List (PLift True))
(Nat : Type 0)
(PLift Nat : Type 1)

Constructor

PLift.up.{u}

将一个证明或值包装起来,以使其类型的宇宙层级增加1。

Fields

down : α

从提升到宇宙的命题或类型中提取一个封装的证明或值。

structure

ULift.{r, s} (α : Type s) : Type (max s r)
ULift.{r, s} (α : Type s) : Type (max s r)

提升一个类型到更高的宇宙层级。

ULift α 会包装一个类型为 α 的值。它不再占用和 α 相同的宇宙层级(即最小的层级)，而是另外接受一个层级参数，并占用两者中的最大值。由此得到的类型可以存在于任何不小于 α 所在层级的宇宙中。

提升操作符的结果宇宙是第一个参数，可以显式写出，同时允许推断 α 的层级。

相关的类型 PLift 可以用来将命题或类型的宇宙提升一级。

Constructor

ULift.up.{r, s}

包装一个值,以提升其类型的宇宙等级。

Fields

down : α

从一个被提升宇宙的类型中提取出被包装的值。